\section{Transformaci\'on de estados del auxiliar estaEnAlgunaTrivia}
 
\subsection{Transformaci\'on de estados del cuerpo principal}

\begin{lstlisting}
bool TelCO:: estaEnAlgunaTrivia(const Usuario u, const Lista<Trivia>& trivias) const{
    Lista <Usuario> us;
\end{lstlisting}
$//E1: Vale\ us == [] $ 
\begin{lstlisting}
    int i=0;
\end{lstlisting}
$//E2: Vale\ us == us@E1 \ylogico i == 0 \\
//Implica Pc: us == [] \ylogico i == 0$
\begin{lstlisting}
    while (i < trivias.longitud()){
\end{lstlisting}
$//Vale\ invariante\ I: 0 \leq i \leq \longitud{trivias} \ylogico \\
//us == (concat (\comp{participantes(trivias_p)}{p \selec [0..i)}) \\
//Funcion\ variante\ V: \longitud{trivias} - i$ \\
\begin{lstlisting}
        us.concatenar(trivias.iesimo(i).participantes());
        i++;
    }
\end{lstlisting}
$//Qc: Vale\ us == (concat (\comp{participantes(trivias_p)}{p \selec [0..\longitud{trivias})}) $ 
\begin{lstlisting}
    return us.pertenece(u);
}
\end{lstlisting}

\subsection{Transformaci\'on de estados del cuerpo del ciclo}
\begin{lstlisting}
while (i < trivias.longitud()){
\end{lstlisting}
$//C1: Vale\ I \ylogico B$
\begin{lstlisting}
  us.concatenar(trivias.iesimo(i).participantes());
\end{lstlisting}
$//C2: Vale\ us == us@C1 ++ participantes(trivias_i@C1) \ylogico i == i@C1$ \\
Ac\'a usamos la poscondici\'on de concatenar, sabiendo que los par\'ametros de entrada cumplen la precondici\'on.
\begin{lstlisting}
  i++;
\end{lstlisting}
$//C3: Vale\ us == us@C2 \ylogico i == i@C2 + 1 $
\begin{lstlisting}
}
\end{lstlisting}

\section{Demostraci\'on del cuerpo del problema}

Suponiendo que el ciclo es correcto respecto de su especificaci\'on, queremos ver que vale la poscondici\'on del problema. //

\begin{problema}{estaEnAlgunaTrivia}{this:TelCO, u:Usuario, ts:[Trivia]}{Bool}{
    \asegura{result == estaEnAlgunaTriviaAux(this, u, ts)}}
\end{problema}

\begin{aux}{estaEnAlgunaTriviaAux}{t:TelCO, u:Usuario, ts:[Trivia]}{Bool}{
    u \in (concat (\comp{participantes(ts_p)}{p \selec [0..\longitud{ts})})}
\end{aux}


$//Qc: Vale\ us == (concat (\comp{participantes(trivias_p)}{p \selec [0..\longitud{trivias})}) $ 
\begin{lstlisting}
    return us.pertenece(u);
}
\end{lstlisting}

La demostraci\'on es bastante directa, solo hace falta usar la especificaci\'on de pertenece y suponerlo correcto respecto de ella.

\begin{problema}{pertenece}{this: [T], e: t}{Bool}{
    \asegura{result == (e \in this)}}
\end{problema}

Luego, probamos que el argumento de return (us.pertenece(u)) cumple la poscondici\'on del problema.

\section{Demostraci\'on del cuerpo del ciclo}

\subsection{$Pc \implica I$}
Supongamos que vale Pc. Queremos ver que vale I. \\
$Pc: us == [] \ylogico i == 0$ \\
$I: 0 \leq i \leq \longitud{trivias} \ylogico \\
//us == (concat (\comp{participantes(trivias_p)}{p \selec [0..i)}) $ \\
Por Pc sabemos que $ us == [] \ylogico i == 0$. Luego, reemplazando en I, queremos ver que: \\
$I: 0 \leq 0 \leq \longitud{trivias} (1) \ylogico \\
//us == (concat (\comp{participantes(trivias_p)}{p \selec [0..0)}) (2)$

Vamos a probar por separado (1) y (2) suponiendo que vale Pc.
(1): Es trivial sabiendo que la longitud de una lista es siempre mayor o igual a 0, y que $ 0 == 0 $ por lo que $ 0 \leq 0 $ \\

(2): Como p va tomando todos los valores en la lista [0..0), que es una lista vac\'ia (propiedad de listas), la lista resultante va a ser tambi\'en vac\'ia. \\
Por lo tanto $us == [] == (concat (\comp{participantes(trivias_p)}{p \selec [0..0)})$ que es lo que quer\'iamos demostrar.

\subsection{La funci\'on variante es estrictamente decreciente}
$Funcion\ variante\ V: \longitud{trivias} - i$
Queremos ver que $ V@C3 < V@C1 $. Sabemos que la longitud de los trivias no se modifica y que $ i@C3 == i@C1 + 1 $ por la transformaci\'on de estados.
Luego, $ V@C1 == \longitud{trivias} - i@C1 > \longitud{trivias} - (i@C1 + 1) == \longitud{trivias} - i@C3 == V@C3 $.

\subsection{$V < 0 \implica \neg B$}
$Funcion\ variante\ V: \longitud{trivias} - i \\
B: i < \longitud{trivias} $ \\
Queremos ver que si $ V < 0 $ el ciclo termina, es decir que vale $ \neg B $. Sabemos que: \\
$ V < 0 \implica \longitud{trivias} - i < 0 \implica i > \longitud{trivias} \implica \neg B $

\subsection{$I \ylogico \neg B \implica Qc $}
$I: 0 \leq i \leq \longitud{trivias} \ylogico \\
us == (concat (\comp{participantes(trivias_p)}{p \selec [0..i)}) \\
B: i < \longitud{trivias} $ \\

$\neg B \implica i \geq \longitud{trivias} $ y a su vez $ I \implica 0 \leq i \leq \longitud{trivias} $. Juntando ambos concluimos \\
que $ \longitud{trivias} \leq i \leq \longitud{trivias} \implica i == \longitud{trivias}$. \\

Reemplazando en el resto de I tenemos que:
$us == (concat (\comp{participantes(trivias_p)}{p \selec [0..\longitud{trivias})})$ \\
que es exactamente Qc.

\subsection{El cuerpo del ciclo preserva el invariante}
Volvamos a la trasnformaci\'on de estados y sigamos las implicaciones.

\begin{lstlisting}
while (i < trivias.longitud()){
\end{lstlisting}
$//C1: Vale\ I \ylogico B \\
//Implica: 0 \leq i < \longitud{trivias} \ylogico \\
//us == (concat (\comp{participantes(trivias_p)}{p \selec [0..i)}) $
\begin{lstlisting}
  us.concatenar(trivias.iesimo(i).participantes());
\end{lstlisting}
$//C2: Vale\ us == us@C1 ++ participantes(trivias_i@C1) \ylogico i == i@C1 \\
//Implica: us == us@C1 ++ parcipatentes(trivias_i)$
\begin{lstlisting}
  i++;
\end{lstlisting}
$//C3: Vale\ us == us@C2 \ylogico i == i@C2 + 1 \\
//Implica: us == us@C1 ++ participantes(trivias_i@C1) \ylogico i == i@C1 + 1$
\begin{lstlisting}
}
\end{lstlisting}

Queremos probar que el invariante vale en C3 suponiendo que val\'ia en C1, y usando las implicaciones de la transformaci\'on de estados.
$I: 0 \leq i \leq \longitud{trivias} (1) \ylogico \\
us == (concat (\comp{participantes(trivias_p)}{p \selec [0..i)}) (2) $ \\

Probaremos por separado (1) y (2). \\
(1): Sabemos que $i@C3 == i@C1 + 1$. Como para entrar al ciclo hac\'ia falta que valiera B, eso quiere decir que $i@C1 < \longitud{trivias}$.
Como tanto $i$ como $\longitud{trivias}$ son enteras, podemos concluir que en C3 $i \leq \longitud{trivias}$.
Como el invariante val\'ia en C1, sabemos tambi\'en que $0 \leq i@C1 \implica 0 \leq i@1 + 1$.\\

(2): En C2, tenemos que \\
$i == i@C1 \ylogico us == us ++ participantes(trivias_i)$ \\
Como el invariante val\'ia en C1, esto implica que \\
$us == (concat (\comp{participantes(trivias_p)}{p \selec [0..i)}) ++ participantes(trivias_i) $\\
Podemos ver que el nuevo elemento tiene la forma de la expresi\'on de la lista por compresi\'on para $p == i$. Entonces, podemos comprimir la lista en esta nueva expresi\'on: \\
$us == (concat (\comp{participantes(trivias_p)}{p \selec [0..i]}) $\\
En C3, $i == i@C2 + 1$, por lo tanto la lista quedar\'ia: \\
$us == (concat (\comp{participantes(trivias_p)}{p \selec [0..i)}) $\\
por propiedad de listas ($[0..i] == [0..i+1)$). Y esta expresi\'on es exactamente (2).
\bigskip


\begin{flushright}
\Huge{$\square$}\end{flushright}